Issue3314.agda:14,5-9
Cannot eliminate fibrant type S1 unless target type is also fibrant
when checking that the pattern base has type S1
